'Weak Dependency Graph [60.0]'
------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ R(2(x1)) -> 2(R(x1))
, R(3(x1)) -> 3(R(x1))
, R(1(x1)) -> L(3(x1))
, 3(L(x1)) -> L(3(x1))
, 2(L(x1)) -> L(2(x1))
, 0(L(x1)) -> 2(R(x1))
, R(b(x1)) -> c(1(b(x1)))
, 3(c(x1)) -> c(1(x1))
, 2(c(1(x1))) -> c(0(R(1(x1))))
, 2(c(0(x1))) -> c(0(0(x1)))}
Details:
We have computed the following set of weak (innermost) dependency pairs:
{ R^#(2(x1)) -> c_0(2^#(R(x1)))
, R^#(3(x1)) -> c_1(3^#(R(x1)))
, R^#(1(x1)) -> c_2(3^#(x1))
, 3^#(L(x1)) -> c_3(3^#(x1))
, 2^#(L(x1)) -> c_4(2^#(x1))
, 0^#(L(x1)) -> c_5(2^#(R(x1)))
, R^#(b(x1)) -> c_6()
, 3^#(c(x1)) -> c_7()
, 2^#(c(1(x1))) -> c_8(0^#(R(1(x1))))
, 2^#(c(0(x1))) -> c_9(0^#(0(x1)))}
The usable rules are:
{ R(2(x1)) -> 2(R(x1))
, R(3(x1)) -> 3(R(x1))
, R(1(x1)) -> L(3(x1))
, 0(L(x1)) -> 2(R(x1))
, R(b(x1)) -> c(1(b(x1)))
, 3(L(x1)) -> L(3(x1))
, 2(L(x1)) -> L(2(x1))
, 3(c(x1)) -> c(1(x1))
, 2(c(1(x1))) -> c(0(R(1(x1))))
, 2(c(0(x1))) -> c(0(0(x1)))}
The estimated dependency graph contains the following edges:
{R^#(2(x1)) -> c_0(2^#(R(x1)))}
==> {2^#(c(0(x1))) -> c_9(0^#(0(x1)))}
{R^#(2(x1)) -> c_0(2^#(R(x1)))}
==> {2^#(c(1(x1))) -> c_8(0^#(R(1(x1))))}
{R^#(2(x1)) -> c_0(2^#(R(x1)))}
==> {2^#(L(x1)) -> c_4(2^#(x1))}
{R^#(3(x1)) -> c_1(3^#(R(x1)))}
==> {3^#(L(x1)) -> c_3(3^#(x1))}
{R^#(3(x1)) -> c_1(3^#(R(x1)))}
==> {3^#(c(x1)) -> c_7()}
{R^#(1(x1)) -> c_2(3^#(x1))}
==> {3^#(L(x1)) -> c_3(3^#(x1))}
{R^#(1(x1)) -> c_2(3^#(x1))}
==> {3^#(c(x1)) -> c_7()}
{3^#(L(x1)) -> c_3(3^#(x1))}
==> {3^#(c(x1)) -> c_7()}
{3^#(L(x1)) -> c_3(3^#(x1))}
==> {3^#(L(x1)) -> c_3(3^#(x1))}
{2^#(L(x1)) -> c_4(2^#(x1))}
==> {2^#(c(0(x1))) -> c_9(0^#(0(x1)))}
{2^#(L(x1)) -> c_4(2^#(x1))}
==> {2^#(c(1(x1))) -> c_8(0^#(R(1(x1))))}
{2^#(L(x1)) -> c_4(2^#(x1))}
==> {2^#(L(x1)) -> c_4(2^#(x1))}
{0^#(L(x1)) -> c_5(2^#(R(x1)))}
==> {2^#(c(0(x1))) -> c_9(0^#(0(x1)))}
{0^#(L(x1)) -> c_5(2^#(R(x1)))}
==> {2^#(c(1(x1))) -> c_8(0^#(R(1(x1))))}
{0^#(L(x1)) -> c_5(2^#(R(x1)))}
==> {2^#(L(x1)) -> c_4(2^#(x1))}
{2^#(c(1(x1))) -> c_8(0^#(R(1(x1))))}
==> {0^#(L(x1)) -> c_5(2^#(R(x1)))}
{2^#(c(0(x1))) -> c_9(0^#(0(x1)))}
==> {0^#(L(x1)) -> c_5(2^#(R(x1)))}
We consider the following path(s):
1) { R^#(3(x1)) -> c_1(3^#(R(x1)))
, 3^#(L(x1)) -> c_3(3^#(x1))
, 3^#(c(x1)) -> c_7()}
The usable rules for this path are the following:
{ R(2(x1)) -> 2(R(x1))
, R(3(x1)) -> 3(R(x1))
, R(1(x1)) -> L(3(x1))
, R(b(x1)) -> c(1(b(x1)))
, 3(L(x1)) -> L(3(x1))
, 2(L(x1)) -> L(2(x1))
, 3(c(x1)) -> c(1(x1))
, 2(c(1(x1))) -> c(0(R(1(x1))))
, 2(c(0(x1))) -> c(0(0(x1)))
, 0(L(x1)) -> 2(R(x1))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ R(2(x1)) -> 2(R(x1))
, R(3(x1)) -> 3(R(x1))
, R(1(x1)) -> L(3(x1))
, R(b(x1)) -> c(1(b(x1)))
, 3(L(x1)) -> L(3(x1))
, 2(L(x1)) -> L(2(x1))
, 3(c(x1)) -> c(1(x1))
, 2(c(1(x1))) -> c(0(R(1(x1))))
, 2(c(0(x1))) -> c(0(0(x1)))
, 0(L(x1)) -> 2(R(x1))
, 3^#(L(x1)) -> c_3(3^#(x1))
, R^#(3(x1)) -> c_1(3^#(R(x1)))
, 3^#(c(x1)) -> c_7()}
Details:
We apply the weight gap principle, strictly orienting the rules
{ 0(L(x1)) -> 2(R(x1))
, 3^#(c(x1)) -> c_7()}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ 0(L(x1)) -> 2(R(x1))
, 3^#(c(x1)) -> c_7()}
Details:
Interpretation Functions:
R(x1) = [1] x1 + [1]
2(x1) = [1] x1 + [0]
3(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
L(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [8]
b(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [9]
R^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
2^#(x1) = [0] x1 + [0]
c_1(x1) = [1] x1 + [0]
3^#(x1) = [1] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [1]
c_4(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{3^#(L(x1)) -> c_3(3^#(x1))}
and weakly orienting the rules
{ 0(L(x1)) -> 2(R(x1))
, 3^#(c(x1)) -> c_7()}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{3^#(L(x1)) -> c_3(3^#(x1))}
Details:
Interpretation Functions:
R(x1) = [1] x1 + [1]
2(x1) = [1] x1 + [0]
3(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
L(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [15]
b(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [1]
R^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
2^#(x1) = [0] x1 + [0]
c_1(x1) = [1] x1 + [1]
3^#(x1) = [1] x1 + [3]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{R^#(3(x1)) -> c_1(3^#(R(x1)))}
and weakly orienting the rules
{ 3^#(L(x1)) -> c_3(3^#(x1))
, 0(L(x1)) -> 2(R(x1))
, 3^#(c(x1)) -> c_7()}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{R^#(3(x1)) -> c_1(3^#(R(x1)))}
Details:
Interpretation Functions:
R(x1) = [1] x1 + [1]
2(x1) = [1] x1 + [0]
3(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
L(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [8]
b(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [1]
R^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
2^#(x1) = [0] x1 + [0]
c_1(x1) = [1] x1 + [0]
3^#(x1) = [1] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [1]
c_4(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{R(b(x1)) -> c(1(b(x1)))}
and weakly orienting the rules
{ R^#(3(x1)) -> c_1(3^#(R(x1)))
, 3^#(L(x1)) -> c_3(3^#(x1))
, 0(L(x1)) -> 2(R(x1))
, 3^#(c(x1)) -> c_7()}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{R(b(x1)) -> c(1(b(x1)))}
Details:
Interpretation Functions:
R(x1) = [1] x1 + [1]
2(x1) = [1] x1 + [0]
3(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
L(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [3]
b(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [0]
R^#(x1) = [1] x1 + [13]
c_0(x1) = [0] x1 + [0]
2^#(x1) = [0] x1 + [0]
c_1(x1) = [1] x1 + [1]
3^#(x1) = [1] x1 + [9]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [1]
c_4(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{R(1(x1)) -> L(3(x1))}
and weakly orienting the rules
{ R(b(x1)) -> c(1(b(x1)))
, R^#(3(x1)) -> c_1(3^#(R(x1)))
, 3^#(L(x1)) -> c_3(3^#(x1))
, 0(L(x1)) -> 2(R(x1))
, 3^#(c(x1)) -> c_7()}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{R(1(x1)) -> L(3(x1))}
Details:
Interpretation Functions:
R(x1) = [1] x1 + [2]
2(x1) = [1] x1 + [0]
3(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [1]
L(x1) = [1] x1 + [2]
0(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [14]
c(x1) = [1] x1 + [0]
R^#(x1) = [1] x1 + [8]
c_0(x1) = [0] x1 + [0]
2^#(x1) = [0] x1 + [0]
c_1(x1) = [1] x1 + [1]
3^#(x1) = [1] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [1]
c_4(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{3(c(x1)) -> c(1(x1))}
and weakly orienting the rules
{ R(1(x1)) -> L(3(x1))
, R(b(x1)) -> c(1(b(x1)))
, R^#(3(x1)) -> c_1(3^#(R(x1)))
, 3^#(L(x1)) -> c_3(3^#(x1))
, 0(L(x1)) -> 2(R(x1))
, 3^#(c(x1)) -> c_7()}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{3(c(x1)) -> c(1(x1))}
Details:
Interpretation Functions:
R(x1) = [1] x1 + [1]
2(x1) = [1] x1 + [0]
3(x1) = [1] x1 + [1]
1(x1) = [1] x1 + [0]
L(x1) = [1] x1 + [0]
0(x1) = [1] x1 + [8]
b(x1) = [1] x1 + [10]
c(x1) = [1] x1 + [0]
R^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
2^#(x1) = [0] x1 + [0]
c_1(x1) = [1] x1 + [0]
3^#(x1) = [1] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ R(2(x1)) -> 2(R(x1))
, R(3(x1)) -> 3(R(x1))
, 3(L(x1)) -> L(3(x1))
, 2(L(x1)) -> L(2(x1))
, 2(c(1(x1))) -> c(0(R(1(x1))))
, 2(c(0(x1))) -> c(0(0(x1)))}
Weak Rules:
{ 3(c(x1)) -> c(1(x1))
, R(1(x1)) -> L(3(x1))
, R(b(x1)) -> c(1(b(x1)))
, R^#(3(x1)) -> c_1(3^#(R(x1)))
, 3^#(L(x1)) -> c_3(3^#(x1))
, 0(L(x1)) -> 2(R(x1))
, 3^#(c(x1)) -> c_7()}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ R(2(x1)) -> 2(R(x1))
, R(3(x1)) -> 3(R(x1))
, 3(L(x1)) -> L(3(x1))
, 2(L(x1)) -> L(2(x1))
, 2(c(1(x1))) -> c(0(R(1(x1))))
, 2(c(0(x1))) -> c(0(0(x1)))}
Weak Rules:
{ 3(c(x1)) -> c(1(x1))
, R(1(x1)) -> L(3(x1))
, R(b(x1)) -> c(1(b(x1)))
, R^#(3(x1)) -> c_1(3^#(R(x1)))
, 3^#(L(x1)) -> c_3(3^#(x1))
, 0(L(x1)) -> 2(R(x1))
, 3^#(c(x1)) -> c_7()}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ 1_0(4) -> 4
, 1_0(5) -> 4
, 1_0(7) -> 4
, 1_0(8) -> 4
, L_0(4) -> 5
, L_0(5) -> 5
, L_0(7) -> 5
, L_0(8) -> 5
, b_0(4) -> 7
, b_0(5) -> 7
, b_0(7) -> 7
, b_0(8) -> 7
, c_0(4) -> 8
, c_0(5) -> 8
, c_0(7) -> 8
, c_0(8) -> 8
, R^#_0(4) -> 9
, R^#_0(5) -> 9
, R^#_0(7) -> 9
, R^#_0(8) -> 9
, 3^#_0(4) -> 13
, 3^#_0(5) -> 13
, 3^#_0(7) -> 13
, 3^#_0(8) -> 13
, c_3_0(13) -> 13
, c_7_0() -> 13}
2) { R^#(3(x1)) -> c_1(3^#(R(x1)))
, 3^#(L(x1)) -> c_3(3^#(x1))}
The usable rules for this path are the following:
{ R(2(x1)) -> 2(R(x1))
, R(3(x1)) -> 3(R(x1))
, R(1(x1)) -> L(3(x1))
, R(b(x1)) -> c(1(b(x1)))
, 3(L(x1)) -> L(3(x1))
, 2(L(x1)) -> L(2(x1))
, 3(c(x1)) -> c(1(x1))
, 2(c(1(x1))) -> c(0(R(1(x1))))
, 2(c(0(x1))) -> c(0(0(x1)))
, 0(L(x1)) -> 2(R(x1))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ R(2(x1)) -> 2(R(x1))
, R(3(x1)) -> 3(R(x1))
, R(1(x1)) -> L(3(x1))
, R(b(x1)) -> c(1(b(x1)))
, 3(L(x1)) -> L(3(x1))
, 2(L(x1)) -> L(2(x1))
, 3(c(x1)) -> c(1(x1))
, 2(c(1(x1))) -> c(0(R(1(x1))))
, 2(c(0(x1))) -> c(0(0(x1)))
, 0(L(x1)) -> 2(R(x1))
, R^#(3(x1)) -> c_1(3^#(R(x1)))
, 3^#(L(x1)) -> c_3(3^#(x1))}
Details:
We apply the weight gap principle, strictly orienting the rules
{3^#(L(x1)) -> c_3(3^#(x1))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{3^#(L(x1)) -> c_3(3^#(x1))}
Details:
Interpretation Functions:
R(x1) = [1] x1 + [1]
2(x1) = [1] x1 + [0]
3(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
L(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [1]
R^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
2^#(x1) = [0] x1 + [0]
c_1(x1) = [1] x1 + [0]
3^#(x1) = [1] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{0(L(x1)) -> 2(R(x1))}
and weakly orienting the rules
{3^#(L(x1)) -> c_3(3^#(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{0(L(x1)) -> 2(R(x1))}
Details:
Interpretation Functions:
R(x1) = [1] x1 + [1]
2(x1) = [1] x1 + [0]
3(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
L(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [15]
b(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [1]
R^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
2^#(x1) = [0] x1 + [0]
c_1(x1) = [1] x1 + [1]
3^#(x1) = [1] x1 + [1]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{R^#(3(x1)) -> c_1(3^#(R(x1)))}
and weakly orienting the rules
{ 0(L(x1)) -> 2(R(x1))
, 3^#(L(x1)) -> c_3(3^#(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{R^#(3(x1)) -> c_1(3^#(R(x1)))}
Details:
Interpretation Functions:
R(x1) = [1] x1 + [1]
2(x1) = [1] x1 + [0]
3(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
L(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [15]
b(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [1]
R^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
2^#(x1) = [0] x1 + [0]
c_1(x1) = [1] x1 + [2]
3^#(x1) = [1] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [1]
c_4(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{R(b(x1)) -> c(1(b(x1)))}
and weakly orienting the rules
{ R^#(3(x1)) -> c_1(3^#(R(x1)))
, 0(L(x1)) -> 2(R(x1))
, 3^#(L(x1)) -> c_3(3^#(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{R(b(x1)) -> c(1(b(x1)))}
Details:
Interpretation Functions:
R(x1) = [1] x1 + [1]
2(x1) = [1] x1 + [0]
3(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
L(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [3]
c(x1) = [1] x1 + [0]
R^#(x1) = [1] x1 + [5]
c_0(x1) = [0] x1 + [0]
2^#(x1) = [0] x1 + [0]
c_1(x1) = [1] x1 + [2]
3^#(x1) = [1] x1 + [2]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [1]
c_4(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{R(1(x1)) -> L(3(x1))}
and weakly orienting the rules
{ R(b(x1)) -> c(1(b(x1)))
, R^#(3(x1)) -> c_1(3^#(R(x1)))
, 0(L(x1)) -> 2(R(x1))
, 3^#(L(x1)) -> c_3(3^#(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{R(1(x1)) -> L(3(x1))}
Details:
Interpretation Functions:
R(x1) = [1] x1 + [1]
2(x1) = [1] x1 + [0]
3(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
L(x1) = [1] x1 + [0]
0(x1) = [1] x1 + [4]
b(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [0]
R^#(x1) = [1] x1 + [3]
c_0(x1) = [0] x1 + [0]
2^#(x1) = [0] x1 + [0]
c_1(x1) = [1] x1 + [1]
3^#(x1) = [1] x1 + [1]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{3(c(x1)) -> c(1(x1))}
and weakly orienting the rules
{ R(1(x1)) -> L(3(x1))
, R(b(x1)) -> c(1(b(x1)))
, R^#(3(x1)) -> c_1(3^#(R(x1)))
, 0(L(x1)) -> 2(R(x1))
, 3^#(L(x1)) -> c_3(3^#(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{3(c(x1)) -> c(1(x1))}
Details:
Interpretation Functions:
R(x1) = [1] x1 + [2]
2(x1) = [1] x1 + [0]
3(x1) = [1] x1 + [2]
1(x1) = [1] x1 + [1]
L(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [14]
c(x1) = [1] x1 + [0]
R^#(x1) = [1] x1 + [14]
c_0(x1) = [0] x1 + [0]
2^#(x1) = [0] x1 + [0]
c_1(x1) = [1] x1 + [0]
3^#(x1) = [1] x1 + [2]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ R(2(x1)) -> 2(R(x1))
, R(3(x1)) -> 3(R(x1))
, 3(L(x1)) -> L(3(x1))
, 2(L(x1)) -> L(2(x1))
, 2(c(1(x1))) -> c(0(R(1(x1))))
, 2(c(0(x1))) -> c(0(0(x1)))}
Weak Rules:
{ 3(c(x1)) -> c(1(x1))
, R(1(x1)) -> L(3(x1))
, R(b(x1)) -> c(1(b(x1)))
, R^#(3(x1)) -> c_1(3^#(R(x1)))
, 0(L(x1)) -> 2(R(x1))
, 3^#(L(x1)) -> c_3(3^#(x1))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ R(2(x1)) -> 2(R(x1))
, R(3(x1)) -> 3(R(x1))
, 3(L(x1)) -> L(3(x1))
, 2(L(x1)) -> L(2(x1))
, 2(c(1(x1))) -> c(0(R(1(x1))))
, 2(c(0(x1))) -> c(0(0(x1)))}
Weak Rules:
{ 3(c(x1)) -> c(1(x1))
, R(1(x1)) -> L(3(x1))
, R(b(x1)) -> c(1(b(x1)))
, R^#(3(x1)) -> c_1(3^#(R(x1)))
, 0(L(x1)) -> 2(R(x1))
, 3^#(L(x1)) -> c_3(3^#(x1))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ 1_0(4) -> 4
, 1_0(5) -> 4
, 1_0(7) -> 4
, 1_0(8) -> 4
, L_0(4) -> 5
, L_0(5) -> 5
, L_0(7) -> 5
, L_0(8) -> 5
, b_0(4) -> 7
, b_0(5) -> 7
, b_0(7) -> 7
, b_0(8) -> 7
, c_0(4) -> 8
, c_0(5) -> 8
, c_0(7) -> 8
, c_0(8) -> 8
, R^#_0(4) -> 9
, R^#_0(5) -> 9
, R^#_0(7) -> 9
, R^#_0(8) -> 9
, 3^#_0(4) -> 13
, 3^#_0(5) -> 13
, 3^#_0(7) -> 13
, 3^#_0(8) -> 13
, c_3_0(13) -> 13}
3) { R^#(2(x1)) -> c_0(2^#(R(x1)))
, 2^#(c(0(x1))) -> c_9(0^#(0(x1)))
, 0^#(L(x1)) -> c_5(2^#(R(x1)))
, 2^#(c(1(x1))) -> c_8(0^#(R(1(x1))))
, 2^#(L(x1)) -> c_4(2^#(x1))}
The usable rules for this path are the following:
{ R(2(x1)) -> 2(R(x1))
, R(3(x1)) -> 3(R(x1))
, R(1(x1)) -> L(3(x1))
, 0(L(x1)) -> 2(R(x1))
, R(b(x1)) -> c(1(b(x1)))
, 3(L(x1)) -> L(3(x1))
, 2(L(x1)) -> L(2(x1))
, 3(c(x1)) -> c(1(x1))
, 2(c(1(x1))) -> c(0(R(1(x1))))
, 2(c(0(x1))) -> c(0(0(x1)))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ R(2(x1)) -> 2(R(x1))
, R(3(x1)) -> 3(R(x1))
, R(1(x1)) -> L(3(x1))
, 0(L(x1)) -> 2(R(x1))
, R(b(x1)) -> c(1(b(x1)))
, 3(L(x1)) -> L(3(x1))
, 2(L(x1)) -> L(2(x1))
, 3(c(x1)) -> c(1(x1))
, 2(c(1(x1))) -> c(0(R(1(x1))))
, 2(c(0(x1))) -> c(0(0(x1)))
, R^#(2(x1)) -> c_0(2^#(R(x1)))
, 2^#(c(0(x1))) -> c_9(0^#(0(x1)))
, 0^#(L(x1)) -> c_5(2^#(R(x1)))
, 2^#(c(1(x1))) -> c_8(0^#(R(1(x1))))
, 2^#(L(x1)) -> c_4(2^#(x1))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ 2^#(c(0(x1))) -> c_9(0^#(0(x1)))
, 2^#(c(1(x1))) -> c_8(0^#(R(1(x1))))
, 2^#(L(x1)) -> c_4(2^#(x1))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ 2^#(c(0(x1))) -> c_9(0^#(0(x1)))
, 2^#(c(1(x1))) -> c_8(0^#(R(1(x1))))
, 2^#(L(x1)) -> c_4(2^#(x1))}
Details:
Interpretation Functions:
R(x1) = [1] x1 + [1]
2(x1) = [1] x1 + [0]
3(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
L(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [1]
R^#(x1) = [1] x1 + [1]
c_0(x1) = [1] x1 + [1]
2^#(x1) = [1] x1 + [15]
c_1(x1) = [0] x1 + [0]
3^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [0]
0^#(x1) = [1] x1 + [0]
c_5(x1) = [1] x1 + [1]
c_6() = [0]
c_7() = [0]
c_8(x1) = [1] x1 + [3]
c_9(x1) = [1] x1 + [1]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{R^#(2(x1)) -> c_0(2^#(R(x1)))}
and weakly orienting the rules
{ 2^#(c(0(x1))) -> c_9(0^#(0(x1)))
, 2^#(c(1(x1))) -> c_8(0^#(R(1(x1))))
, 2^#(L(x1)) -> c_4(2^#(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{R^#(2(x1)) -> c_0(2^#(R(x1)))}
Details:
Interpretation Functions:
R(x1) = [1] x1 + [1]
2(x1) = [1] x1 + [0]
3(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
L(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [1]
R^#(x1) = [1] x1 + [12]
c_0(x1) = [1] x1 + [8]
2^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
3^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [1]
0^#(x1) = [1] x1 + [0]
c_5(x1) = [1] x1 + [0]
c_6() = [0]
c_7() = [0]
c_8(x1) = [1] x1 + [0]
c_9(x1) = [1] x1 + [1]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{0(L(x1)) -> 2(R(x1))}
and weakly orienting the rules
{ R^#(2(x1)) -> c_0(2^#(R(x1)))
, 2^#(c(0(x1))) -> c_9(0^#(0(x1)))
, 2^#(c(1(x1))) -> c_8(0^#(R(1(x1))))
, 2^#(L(x1)) -> c_4(2^#(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{0(L(x1)) -> 2(R(x1))}
Details:
Interpretation Functions:
R(x1) = [1] x1 + [1]
2(x1) = [1] x1 + [0]
3(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
L(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [1]
R^#(x1) = [1] x1 + [9]
c_0(x1) = [1] x1 + [1]
2^#(x1) = [1] x1 + [5]
c_1(x1) = [0] x1 + [0]
3^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [1]
0^#(x1) = [1] x1 + [0]
c_5(x1) = [1] x1 + [1]
c_6() = [0]
c_7() = [0]
c_8(x1) = [1] x1 + [0]
c_9(x1) = [1] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{0^#(L(x1)) -> c_5(2^#(R(x1)))}
and weakly orienting the rules
{ 0(L(x1)) -> 2(R(x1))
, R^#(2(x1)) -> c_0(2^#(R(x1)))
, 2^#(c(0(x1))) -> c_9(0^#(0(x1)))
, 2^#(c(1(x1))) -> c_8(0^#(R(1(x1))))
, 2^#(L(x1)) -> c_4(2^#(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{0^#(L(x1)) -> c_5(2^#(R(x1)))}
Details:
Interpretation Functions:
R(x1) = [1] x1 + [1]
2(x1) = [1] x1 + [0]
3(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
L(x1) = [1] x1 + [10]
0(x1) = [1] x1 + [2]
b(x1) = [1] x1 + [8]
c(x1) = [1] x1 + [13]
R^#(x1) = [1] x1 + [9]
c_0(x1) = [1] x1 + [4]
2^#(x1) = [1] x1 + [3]
c_1(x1) = [0] x1 + [0]
3^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [0]
0^#(x1) = [1] x1 + [3]
c_5(x1) = [1] x1 + [5]
c_6() = [0]
c_7() = [0]
c_8(x1) = [1] x1 + [5]
c_9(x1) = [1] x1 + [12]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{R(1(x1)) -> L(3(x1))}
and weakly orienting the rules
{ 0^#(L(x1)) -> c_5(2^#(R(x1)))
, 0(L(x1)) -> 2(R(x1))
, R^#(2(x1)) -> c_0(2^#(R(x1)))
, 2^#(c(0(x1))) -> c_9(0^#(0(x1)))
, 2^#(c(1(x1))) -> c_8(0^#(R(1(x1))))
, 2^#(L(x1)) -> c_4(2^#(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{R(1(x1)) -> L(3(x1))}
Details:
Interpretation Functions:
R(x1) = [1] x1 + [0]
2(x1) = [1] x1 + [0]
3(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [4]
L(x1) = [1] x1 + [0]
0(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [0]
R^#(x1) = [1] x1 + [9]
c_0(x1) = [1] x1 + [0]
2^#(x1) = [1] x1 + [1]
c_1(x1) = [0] x1 + [0]
3^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [0]
0^#(x1) = [1] x1 + [1]
c_5(x1) = [1] x1 + [0]
c_6() = [0]
c_7() = [0]
c_8(x1) = [1] x1 + [0]
c_9(x1) = [1] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ 2(c(1(x1))) -> c(0(R(1(x1))))
, 2(c(0(x1))) -> c(0(0(x1)))}
and weakly orienting the rules
{ R(1(x1)) -> L(3(x1))
, 0^#(L(x1)) -> c_5(2^#(R(x1)))
, 0(L(x1)) -> 2(R(x1))
, R^#(2(x1)) -> c_0(2^#(R(x1)))
, 2^#(c(0(x1))) -> c_9(0^#(0(x1)))
, 2^#(c(1(x1))) -> c_8(0^#(R(1(x1))))
, 2^#(L(x1)) -> c_4(2^#(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ 2(c(1(x1))) -> c(0(R(1(x1))))
, 2(c(0(x1))) -> c(0(0(x1)))}
Details:
Interpretation Functions:
R(x1) = [1] x1 + [0]
2(x1) = [1] x1 + [8]
3(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [4]
L(x1) = [1] x1 + [4]
0(x1) = [1] x1 + [4]
b(x1) = [1] x1 + [1]
c(x1) = [1] x1 + [14]
R^#(x1) = [1] x1 + [9]
c_0(x1) = [1] x1 + [0]
2^#(x1) = [1] x1 + [2]
c_1(x1) = [0] x1 + [0]
3^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [1]
0^#(x1) = [1] x1 + [12]
c_5(x1) = [1] x1 + [0]
c_6() = [0]
c_7() = [0]
c_8(x1) = [1] x1 + [0]
c_9(x1) = [1] x1 + [4]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ R(2(x1)) -> 2(R(x1))
, R(3(x1)) -> 3(R(x1))
, R(b(x1)) -> c(1(b(x1)))
, 3(L(x1)) -> L(3(x1))
, 2(L(x1)) -> L(2(x1))
, 3(c(x1)) -> c(1(x1))}
Weak Rules:
{ 2(c(1(x1))) -> c(0(R(1(x1))))
, 2(c(0(x1))) -> c(0(0(x1)))
, R(1(x1)) -> L(3(x1))
, 0^#(L(x1)) -> c_5(2^#(R(x1)))
, 0(L(x1)) -> 2(R(x1))
, R^#(2(x1)) -> c_0(2^#(R(x1)))
, 2^#(c(0(x1))) -> c_9(0^#(0(x1)))
, 2^#(c(1(x1))) -> c_8(0^#(R(1(x1))))
, 2^#(L(x1)) -> c_4(2^#(x1))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ R(2(x1)) -> 2(R(x1))
, R(3(x1)) -> 3(R(x1))
, R(b(x1)) -> c(1(b(x1)))
, 3(L(x1)) -> L(3(x1))
, 2(L(x1)) -> L(2(x1))
, 3(c(x1)) -> c(1(x1))}
Weak Rules:
{ 2(c(1(x1))) -> c(0(R(1(x1))))
, 2(c(0(x1))) -> c(0(0(x1)))
, R(1(x1)) -> L(3(x1))
, 0^#(L(x1)) -> c_5(2^#(R(x1)))
, 0(L(x1)) -> 2(R(x1))
, R^#(2(x1)) -> c_0(2^#(R(x1)))
, 2^#(c(0(x1))) -> c_9(0^#(0(x1)))
, 2^#(c(1(x1))) -> c_8(0^#(R(1(x1))))
, 2^#(L(x1)) -> c_4(2^#(x1))}
Details:
The problem is Match-bounded by 5.
The enriched problem is compatible with the following automaton:
{ R_0(2) -> 4
, R_1(2) -> 10
, R_1(6) -> 17
, R_1(8) -> 12
, R_1(15) -> 14
, R_2(2) -> 32
, R_2(7) -> 33
, R_2(19) -> 23
, R_2(20) -> 27
, R_2(21) -> 25
, R_2(30) -> 29
, R_2(47) -> 46
, R_3(2) -> 68
, R_3(6) -> 54
, R_3(7) -> 55
, R_3(38) -> 52
, R_3(39) -> 42
, R_3(40) -> 44
, R_3(50) -> 49
, R_3(56) -> 60
, R_3(57) -> 62
, R_3(58) -> 64
, R_3(67) -> 66
, R_4(6) -> 69
, R_4(15) -> 84
, R_4(34) -> 70
, R_4(57) -> 75
, R_4(58) -> 77
, R_4(72) -> 79
, R_4(82) -> 81
, R_4(86) -> 88
, R_5(34) -> 92
, R_5(86) -> 95
, 3_0(2) -> 8
, 3_1(2) -> 19
, 3_1(7) -> 21
, 3_1(10) -> 12
, 3_2(2) -> 56
, 3_2(6) -> 39
, 3_2(7) -> 40
, 3_2(19) -> 36
, 3_2(32) -> 23
, 3_2(33) -> 25
, 3_3(6) -> 57
, 3_3(15) -> 72
, 3_3(34) -> 58
, 3_3(35) -> 73
, 3_3(40) -> 71
, 3_3(54) -> 42
, 3_3(55) -> 44
, 3_3(56) -> 93
, 3_3(68) -> 60
, 3_4(34) -> 86
, 3_4(69) -> 62
, 3_4(69) -> 75
, 3_4(70) -> 64
, 3_4(70) -> 77
, 3_4(73) -> 85
, 3_4(84) -> 79
, 3_5(92) -> 88
, 3_5(92) -> 95
, 1_0(2) -> 2
, 1_1(2) -> 15
, 1_1(7) -> 6
, 1_2(2) -> 47
, 1_2(6) -> 20
, 1_2(7) -> 30
, 1_2(15) -> 37
, 1_2(35) -> 34
, 1_3(6) -> 50
, 1_3(15) -> 67
, 1_3(34) -> 38
, 1_4(34) -> 82
, L_0(2) -> 2
, L_0(8) -> 4
, L_1(19) -> 8
, L_1(19) -> 10
, L_1(19) -> 14
, L_1(19) -> 19
, L_1(19) -> 32
, L_1(19) -> 56
, L_1(19) -> 68
, L_1(21) -> 17
, L_2(36) -> 12
, L_2(36) -> 23
, L_2(36) -> 36
, L_2(36) -> 60
, L_2(36) -> 93
, L_2(39) -> 27
, L_2(40) -> 29
, L_2(40) -> 54
, L_2(40) -> 69
, L_2(56) -> 46
, L_2(56) -> 84
, L_3(57) -> 49
, L_3(58) -> 52
, L_3(71) -> 42
, L_3(71) -> 62
, L_3(71) -> 75
, L_3(72) -> 66
, L_3(73) -> 70
, L_3(73) -> 92
, L_3(93) -> 79
, L_4(85) -> 64
, L_4(85) -> 77
, L_4(85) -> 88
, L_4(85) -> 95
, L_4(86) -> 81
, b_0(2) -> 2
, b_1(2) -> 7
, b_2(2) -> 35
, c_0(2) -> 2
, c_1(6) -> 4
, c_1(6) -> 10
, c_1(6) -> 32
, c_1(6) -> 68
, c_1(15) -> 8
, c_1(15) -> 19
, c_1(15) -> 56
, c_2(20) -> 12
, c_2(20) -> 23
, c_2(20) -> 60
, c_2(34) -> 33
, c_2(34) -> 55
, c_2(37) -> 36
, c_2(37) -> 93
, c_3(38) -> 25
, c_3(38) -> 44
, R^#_0(2) -> 1
, 2^#_0(2) -> 1
, 2^#_0(4) -> 3
, 2^#_0(8) -> 18
, 2^#_1(10) -> 9
, 2^#_1(12) -> 11
, 2^#_1(19) -> 31
, 2^#_2(23) -> 22
, 2^#_2(25) -> 24
, 2^#_2(36) -> 53
, 2^#_3(36) -> 89
, 2^#_3(42) -> 41
, 2^#_3(44) -> 43
, 2^#_3(60) -> 59
, 2^#_3(62) -> 61
, 2^#_3(64) -> 63
, 2^#_3(71) -> 83
, 2^#_4(71) -> 90
, 2^#_4(75) -> 74
, 2^#_4(77) -> 76
, 2^#_4(79) -> 78
, 2^#_4(85) -> 91
, 2^#_4(88) -> 87
, 2^#_4(93) -> 96
, 2^#_5(85) -> 97
, 2^#_5(95) -> 94
, c_4_0(1) -> 1
, c_4_0(18) -> 3
, c_4_1(31) -> 9
, c_4_1(31) -> 18
, c_4_1(31) -> 31
, c_4_2(53) -> 11
, c_4_2(53) -> 22
, c_4_2(53) -> 53
, c_4_3(83) -> 41
, c_4_3(83) -> 61
, c_4_3(89) -> 59
, c_4_3(89) -> 89
, c_4_3(89) -> 96
, c_4_4(90) -> 74
, c_4_4(91) -> 63
, c_4_4(91) -> 76
, c_4_4(91) -> 87
, c_4_4(96) -> 78
, c_4_5(97) -> 94
, 0^#_0(2) -> 1
, 0^#_0(4) -> 5
, 0^#_1(14) -> 13
, 0^#_1(17) -> 16
, 0^#_2(27) -> 26
, 0^#_2(29) -> 28
, 0^#_2(46) -> 45
, 0^#_3(49) -> 48
, 0^#_3(52) -> 51
, 0^#_3(66) -> 65
, 0^#_4(81) -> 80
, c_5_0(3) -> 1
, c_5_1(9) -> 1
, c_5_1(11) -> 5
, c_5_2(22) -> 13
, c_5_2(24) -> 16
, c_5_3(41) -> 26
, c_5_3(43) -> 28
, c_5_3(59) -> 45
, c_5_3(61) -> 48
, c_5_3(63) -> 51
, c_5_4(74) -> 48
, c_5_4(76) -> 51
, c_5_4(78) -> 65
, c_5_4(87) -> 80
, c_5_5(94) -> 80
, c_8_0(5) -> 1
, c_8_1(13) -> 1
, c_8_1(13) -> 18
, c_8_1(16) -> 3
, c_8_2(26) -> 11
, c_8_2(28) -> 9
, c_8_2(45) -> 31
, c_8_3(48) -> 22
, c_8_3(48) -> 59
, c_8_3(51) -> 24
, c_8_3(51) -> 43
, c_8_3(65) -> 53
, c_8_3(65) -> 89
, c_8_3(65) -> 96
, c_8_4(80) -> 43}
4) {R^#(3(x1)) -> c_1(3^#(R(x1)))}
The usable rules for this path are the following:
{ R(2(x1)) -> 2(R(x1))
, R(3(x1)) -> 3(R(x1))
, R(1(x1)) -> L(3(x1))
, R(b(x1)) -> c(1(b(x1)))
, 3(L(x1)) -> L(3(x1))
, 2(L(x1)) -> L(2(x1))
, 3(c(x1)) -> c(1(x1))
, 2(c(1(x1))) -> c(0(R(1(x1))))
, 2(c(0(x1))) -> c(0(0(x1)))
, 0(L(x1)) -> 2(R(x1))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ R(2(x1)) -> 2(R(x1))
, R(3(x1)) -> 3(R(x1))
, R(1(x1)) -> L(3(x1))
, R(b(x1)) -> c(1(b(x1)))
, 3(L(x1)) -> L(3(x1))
, 2(L(x1)) -> L(2(x1))
, 3(c(x1)) -> c(1(x1))
, 2(c(1(x1))) -> c(0(R(1(x1))))
, 2(c(0(x1))) -> c(0(0(x1)))
, 0(L(x1)) -> 2(R(x1))
, R^#(3(x1)) -> c_1(3^#(R(x1)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{0(L(x1)) -> 2(R(x1))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{0(L(x1)) -> 2(R(x1))}
Details:
Interpretation Functions:
R(x1) = [1] x1 + [1]
2(x1) = [1] x1 + [0]
3(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
L(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [9]
b(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [1]
R^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
2^#(x1) = [0] x1 + [0]
c_1(x1) = [1] x1 + [0]
3^#(x1) = [1] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{R^#(3(x1)) -> c_1(3^#(R(x1)))}
and weakly orienting the rules
{0(L(x1)) -> 2(R(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{R^#(3(x1)) -> c_1(3^#(R(x1)))}
Details:
Interpretation Functions:
R(x1) = [1] x1 + [1]
2(x1) = [1] x1 + [0]
3(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
L(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [1]
R^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
2^#(x1) = [0] x1 + [0]
c_1(x1) = [1] x1 + [1]
3^#(x1) = [1] x1 + [3]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{R(1(x1)) -> L(3(x1))}
and weakly orienting the rules
{ R^#(3(x1)) -> c_1(3^#(R(x1)))
, 0(L(x1)) -> 2(R(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{R(1(x1)) -> L(3(x1))}
Details:
Interpretation Functions:
R(x1) = [1] x1 + [1]
2(x1) = [1] x1 + [0]
3(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [3]
L(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [4]
c(x1) = [1] x1 + [0]
R^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
2^#(x1) = [0] x1 + [0]
c_1(x1) = [1] x1 + [0]
3^#(x1) = [1] x1 + [1]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{R(b(x1)) -> c(1(b(x1)))}
and weakly orienting the rules
{ R(1(x1)) -> L(3(x1))
, R^#(3(x1)) -> c_1(3^#(R(x1)))
, 0(L(x1)) -> 2(R(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{R(b(x1)) -> c(1(b(x1)))}
Details:
Interpretation Functions:
R(x1) = [1] x1 + [1]
2(x1) = [1] x1 + [0]
3(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
L(x1) = [1] x1 + [0]
0(x1) = [1] x1 + [4]
b(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [0]
R^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
2^#(x1) = [0] x1 + [0]
c_1(x1) = [1] x1 + [0]
3^#(x1) = [1] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{3(c(x1)) -> c(1(x1))}
and weakly orienting the rules
{ R(b(x1)) -> c(1(b(x1)))
, R(1(x1)) -> L(3(x1))
, R^#(3(x1)) -> c_1(3^#(R(x1)))
, 0(L(x1)) -> 2(R(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{3(c(x1)) -> c(1(x1))}
Details:
Interpretation Functions:
R(x1) = [1] x1 + [2]
2(x1) = [1] x1 + [0]
3(x1) = [1] x1 + [1]
1(x1) = [1] x1 + [0]
L(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [3]
b(x1) = [1] x1 + [2]
c(x1) = [1] x1 + [0]
R^#(x1) = [1] x1 + [15]
c_0(x1) = [0] x1 + [0]
2^#(x1) = [0] x1 + [0]
c_1(x1) = [1] x1 + [2]
3^#(x1) = [1] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ R(2(x1)) -> 2(R(x1))
, R(3(x1)) -> 3(R(x1))
, 3(L(x1)) -> L(3(x1))
, 2(L(x1)) -> L(2(x1))
, 2(c(1(x1))) -> c(0(R(1(x1))))
, 2(c(0(x1))) -> c(0(0(x1)))}
Weak Rules:
{ 3(c(x1)) -> c(1(x1))
, R(b(x1)) -> c(1(b(x1)))
, R(1(x1)) -> L(3(x1))
, R^#(3(x1)) -> c_1(3^#(R(x1)))
, 0(L(x1)) -> 2(R(x1))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ R(2(x1)) -> 2(R(x1))
, R(3(x1)) -> 3(R(x1))
, 3(L(x1)) -> L(3(x1))
, 2(L(x1)) -> L(2(x1))
, 2(c(1(x1))) -> c(0(R(1(x1))))
, 2(c(0(x1))) -> c(0(0(x1)))}
Weak Rules:
{ 3(c(x1)) -> c(1(x1))
, R(b(x1)) -> c(1(b(x1)))
, R(1(x1)) -> L(3(x1))
, R^#(3(x1)) -> c_1(3^#(R(x1)))
, 0(L(x1)) -> 2(R(x1))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ 1_0(4) -> 4
, 1_0(5) -> 4
, 1_0(7) -> 4
, 1_0(8) -> 4
, L_0(4) -> 5
, L_0(5) -> 5
, L_0(7) -> 5
, L_0(8) -> 5
, b_0(4) -> 7
, b_0(5) -> 7
, b_0(7) -> 7
, b_0(8) -> 7
, c_0(4) -> 8
, c_0(5) -> 8
, c_0(7) -> 8
, c_0(8) -> 8
, R^#_0(4) -> 9
, R^#_0(5) -> 9
, R^#_0(7) -> 9
, R^#_0(8) -> 9
, 3^#_0(4) -> 13
, 3^#_0(5) -> 13
, 3^#_0(7) -> 13
, 3^#_0(8) -> 13}
5) {R^#(2(x1)) -> c_0(2^#(R(x1)))}
The usable rules for this path are the following:
{ R(2(x1)) -> 2(R(x1))
, R(3(x1)) -> 3(R(x1))
, R(1(x1)) -> L(3(x1))
, R(b(x1)) -> c(1(b(x1)))
, 3(L(x1)) -> L(3(x1))
, 2(L(x1)) -> L(2(x1))
, 3(c(x1)) -> c(1(x1))
, 2(c(1(x1))) -> c(0(R(1(x1))))
, 2(c(0(x1))) -> c(0(0(x1)))
, 0(L(x1)) -> 2(R(x1))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ R(2(x1)) -> 2(R(x1))
, R(3(x1)) -> 3(R(x1))
, R(1(x1)) -> L(3(x1))
, R(b(x1)) -> c(1(b(x1)))
, 3(L(x1)) -> L(3(x1))
, 2(L(x1)) -> L(2(x1))
, 3(c(x1)) -> c(1(x1))
, 2(c(1(x1))) -> c(0(R(1(x1))))
, 2(c(0(x1))) -> c(0(0(x1)))
, 0(L(x1)) -> 2(R(x1))
, R^#(2(x1)) -> c_0(2^#(R(x1)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{0(L(x1)) -> 2(R(x1))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{0(L(x1)) -> 2(R(x1))}
Details:
Interpretation Functions:
R(x1) = [1] x1 + [1]
2(x1) = [1] x1 + [0]
3(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
L(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [8]
b(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [1]
R^#(x1) = [1] x1 + [1]
c_0(x1) = [1] x1 + [0]
2^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
3^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{R^#(2(x1)) -> c_0(2^#(R(x1)))}
and weakly orienting the rules
{0(L(x1)) -> 2(R(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{R^#(2(x1)) -> c_0(2^#(R(x1)))}
Details:
Interpretation Functions:
R(x1) = [1] x1 + [1]
2(x1) = [1] x1 + [0]
3(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
L(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [12]
b(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [1]
R^#(x1) = [1] x1 + [9]
c_0(x1) = [1] x1 + [0]
2^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
3^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{R(b(x1)) -> c(1(b(x1)))}
and weakly orienting the rules
{ R^#(2(x1)) -> c_0(2^#(R(x1)))
, 0(L(x1)) -> 2(R(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{R(b(x1)) -> c(1(b(x1)))}
Details:
Interpretation Functions:
R(x1) = [1] x1 + [1]
2(x1) = [1] x1 + [0]
3(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
L(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [0]
R^#(x1) = [1] x1 + [13]
c_0(x1) = [1] x1 + [0]
2^#(x1) = [1] x1 + [7]
c_1(x1) = [0] x1 + [0]
3^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{R(1(x1)) -> L(3(x1))}
and weakly orienting the rules
{ R(b(x1)) -> c(1(b(x1)))
, R^#(2(x1)) -> c_0(2^#(R(x1)))
, 0(L(x1)) -> 2(R(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{R(1(x1)) -> L(3(x1))}
Details:
Interpretation Functions:
R(x1) = [1] x1 + [1]
2(x1) = [1] x1 + [0]
3(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
L(x1) = [1] x1 + [0]
0(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [4]
c(x1) = [1] x1 + [0]
R^#(x1) = [1] x1 + [3]
c_0(x1) = [1] x1 + [0]
2^#(x1) = [1] x1 + [1]
c_1(x1) = [0] x1 + [0]
3^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{2(c(0(x1))) -> c(0(0(x1)))}
and weakly orienting the rules
{ R(1(x1)) -> L(3(x1))
, R(b(x1)) -> c(1(b(x1)))
, R^#(2(x1)) -> c_0(2^#(R(x1)))
, 0(L(x1)) -> 2(R(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{2(c(0(x1))) -> c(0(0(x1)))}
Details:
Interpretation Functions:
R(x1) = [1] x1 + [2]
2(x1) = [1] x1 + [1]
3(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [1]
L(x1) = [1] x1 + [3]
0(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [0]
R^#(x1) = [1] x1 + [15]
c_0(x1) = [1] x1 + [0]
2^#(x1) = [1] x1 + [14]
c_1(x1) = [0] x1 + [0]
3^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ R(2(x1)) -> 2(R(x1))
, R(3(x1)) -> 3(R(x1))
, 3(L(x1)) -> L(3(x1))
, 2(L(x1)) -> L(2(x1))
, 3(c(x1)) -> c(1(x1))
, 2(c(1(x1))) -> c(0(R(1(x1))))}
Weak Rules:
{ 2(c(0(x1))) -> c(0(0(x1)))
, R(1(x1)) -> L(3(x1))
, R(b(x1)) -> c(1(b(x1)))
, R^#(2(x1)) -> c_0(2^#(R(x1)))
, 0(L(x1)) -> 2(R(x1))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ R(2(x1)) -> 2(R(x1))
, R(3(x1)) -> 3(R(x1))
, 3(L(x1)) -> L(3(x1))
, 2(L(x1)) -> L(2(x1))
, 3(c(x1)) -> c(1(x1))
, 2(c(1(x1))) -> c(0(R(1(x1))))}
Weak Rules:
{ 2(c(0(x1))) -> c(0(0(x1)))
, R(1(x1)) -> L(3(x1))
, R(b(x1)) -> c(1(b(x1)))
, R^#(2(x1)) -> c_0(2^#(R(x1)))
, 0(L(x1)) -> 2(R(x1))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ 1_0(2) -> 2
, L_0(2) -> 2
, b_0(2) -> 2
, c_0(2) -> 2
, R^#_0(2) -> 1
, 2^#_0(2) -> 1}
6) { R^#(3(x1)) -> c_1(3^#(R(x1)))
, 3^#(c(x1)) -> c_7()}
The usable rules for this path are the following:
{ R(2(x1)) -> 2(R(x1))
, R(3(x1)) -> 3(R(x1))
, R(1(x1)) -> L(3(x1))
, R(b(x1)) -> c(1(b(x1)))
, 3(L(x1)) -> L(3(x1))
, 2(L(x1)) -> L(2(x1))
, 3(c(x1)) -> c(1(x1))
, 2(c(1(x1))) -> c(0(R(1(x1))))
, 2(c(0(x1))) -> c(0(0(x1)))
, 0(L(x1)) -> 2(R(x1))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ R(2(x1)) -> 2(R(x1))
, R(3(x1)) -> 3(R(x1))
, R(1(x1)) -> L(3(x1))
, R(b(x1)) -> c(1(b(x1)))
, 3(L(x1)) -> L(3(x1))
, 2(L(x1)) -> L(2(x1))
, 3(c(x1)) -> c(1(x1))
, 2(c(1(x1))) -> c(0(R(1(x1))))
, 2(c(0(x1))) -> c(0(0(x1)))
, 0(L(x1)) -> 2(R(x1))
, R^#(3(x1)) -> c_1(3^#(R(x1)))
, 3^#(c(x1)) -> c_7()}
Details:
We apply the weight gap principle, strictly orienting the rules
{ 0(L(x1)) -> 2(R(x1))
, 3^#(c(x1)) -> c_7()}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ 0(L(x1)) -> 2(R(x1))
, 3^#(c(x1)) -> c_7()}
Details:
Interpretation Functions:
R(x1) = [1] x1 + [1]
2(x1) = [1] x1 + [0]
3(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
L(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [3]
b(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [9]
R^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
2^#(x1) = [0] x1 + [0]
c_1(x1) = [1] x1 + [0]
3^#(x1) = [1] x1 + [4]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{R^#(3(x1)) -> c_1(3^#(R(x1)))}
and weakly orienting the rules
{ 0(L(x1)) -> 2(R(x1))
, 3^#(c(x1)) -> c_7()}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{R^#(3(x1)) -> c_1(3^#(R(x1)))}
Details:
Interpretation Functions:
R(x1) = [1] x1 + [1]
2(x1) = [1] x1 + [0]
3(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
L(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [3]
b(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [9]
R^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
2^#(x1) = [0] x1 + [0]
c_1(x1) = [1] x1 + [0]
3^#(x1) = [1] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{R(1(x1)) -> L(3(x1))}
and weakly orienting the rules
{ R^#(3(x1)) -> c_1(3^#(R(x1)))
, 0(L(x1)) -> 2(R(x1))
, 3^#(c(x1)) -> c_7()}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{R(1(x1)) -> L(3(x1))}
Details:
Interpretation Functions:
R(x1) = [1] x1 + [0]
2(x1) = [1] x1 + [0]
3(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [4]
L(x1) = [1] x1 + [0]
0(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [12]
c(x1) = [1] x1 + [0]
R^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
2^#(x1) = [0] x1 + [0]
c_1(x1) = [1] x1 + [5]
3^#(x1) = [1] x1 + [4]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{R(b(x1)) -> c(1(b(x1)))}
and weakly orienting the rules
{ R(1(x1)) -> L(3(x1))
, R^#(3(x1)) -> c_1(3^#(R(x1)))
, 0(L(x1)) -> 2(R(x1))
, 3^#(c(x1)) -> c_7()}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{R(b(x1)) -> c(1(b(x1)))}
Details:
Interpretation Functions:
R(x1) = [1] x1 + [1]
2(x1) = [1] x1 + [0]
3(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
L(x1) = [1] x1 + [0]
0(x1) = [1] x1 + [2]
b(x1) = [1] x1 + [2]
c(x1) = [1] x1 + [0]
R^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
2^#(x1) = [0] x1 + [0]
c_1(x1) = [1] x1 + [1]
3^#(x1) = [1] x1 + [4]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{3(c(x1)) -> c(1(x1))}
and weakly orienting the rules
{ R(b(x1)) -> c(1(b(x1)))
, R(1(x1)) -> L(3(x1))
, R^#(3(x1)) -> c_1(3^#(R(x1)))
, 0(L(x1)) -> 2(R(x1))
, 3^#(c(x1)) -> c_7()}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{3(c(x1)) -> c(1(x1))}
Details:
Interpretation Functions:
R(x1) = [1] x1 + [4]
2(x1) = [1] x1 + [0]
3(x1) = [1] x1 + [8]
1(x1) = [1] x1 + [4]
L(x1) = [1] x1 + [0]
0(x1) = [1] x1 + [8]
b(x1) = [1] x1 + [1]
c(x1) = [1] x1 + [0]
R^#(x1) = [1] x1 + [0]
c_0(x1) = [0] x1 + [0]
2^#(x1) = [0] x1 + [0]
c_1(x1) = [1] x1 + [1]
3^#(x1) = [1] x1 + [1]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ R(2(x1)) -> 2(R(x1))
, R(3(x1)) -> 3(R(x1))
, 3(L(x1)) -> L(3(x1))
, 2(L(x1)) -> L(2(x1))
, 2(c(1(x1))) -> c(0(R(1(x1))))
, 2(c(0(x1))) -> c(0(0(x1)))}
Weak Rules:
{ 3(c(x1)) -> c(1(x1))
, R(b(x1)) -> c(1(b(x1)))
, R(1(x1)) -> L(3(x1))
, R^#(3(x1)) -> c_1(3^#(R(x1)))
, 0(L(x1)) -> 2(R(x1))
, 3^#(c(x1)) -> c_7()}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ R(2(x1)) -> 2(R(x1))
, R(3(x1)) -> 3(R(x1))
, 3(L(x1)) -> L(3(x1))
, 2(L(x1)) -> L(2(x1))
, 2(c(1(x1))) -> c(0(R(1(x1))))
, 2(c(0(x1))) -> c(0(0(x1)))}
Weak Rules:
{ 3(c(x1)) -> c(1(x1))
, R(b(x1)) -> c(1(b(x1)))
, R(1(x1)) -> L(3(x1))
, R^#(3(x1)) -> c_1(3^#(R(x1)))
, 0(L(x1)) -> 2(R(x1))
, 3^#(c(x1)) -> c_7()}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ 1_0(4) -> 4
, 1_0(5) -> 4
, 1_0(7) -> 4
, 1_0(8) -> 4
, L_0(4) -> 5
, L_0(5) -> 5
, L_0(7) -> 5
, L_0(8) -> 5
, b_0(4) -> 7
, b_0(5) -> 7
, b_0(7) -> 7
, b_0(8) -> 7
, c_0(4) -> 8
, c_0(5) -> 8
, c_0(7) -> 8
, c_0(8) -> 8
, R^#_0(4) -> 9
, R^#_0(5) -> 9
, R^#_0(7) -> 9
, R^#_0(8) -> 9
, 3^#_0(4) -> 13
, 3^#_0(5) -> 13
, 3^#_0(7) -> 13
, 3^#_0(8) -> 13
, c_7_0() -> 13}
7) { R^#(1(x1)) -> c_2(3^#(x1))
, 3^#(L(x1)) -> c_3(3^#(x1))
, 3^#(c(x1)) -> c_7()}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
R(x1) = [0] x1 + [0]
2(x1) = [0] x1 + [0]
3(x1) = [0] x1 + [0]
1(x1) = [0] x1 + [0]
L(x1) = [0] x1 + [0]
0(x1) = [0] x1 + [0]
b(x1) = [0] x1 + [0]
c(x1) = [0] x1 + [0]
R^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
2^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
3^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {3^#(c(x1)) -> c_7()}
Weak Rules:
{ 3^#(L(x1)) -> c_3(3^#(x1))
, R^#(1(x1)) -> c_2(3^#(x1))}
Details:
We apply the weight gap principle, strictly orienting the rules
{3^#(c(x1)) -> c_7()}
and weakly orienting the rules
{ 3^#(L(x1)) -> c_3(3^#(x1))
, R^#(1(x1)) -> c_2(3^#(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{3^#(c(x1)) -> c_7()}
Details:
Interpretation Functions:
R(x1) = [0] x1 + [0]
2(x1) = [0] x1 + [0]
3(x1) = [0] x1 + [0]
1(x1) = [1] x1 + [0]
L(x1) = [1] x1 + [0]
0(x1) = [0] x1 + [0]
b(x1) = [0] x1 + [0]
c(x1) = [1] x1 + [0]
R^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
2^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
3^#(x1) = [1] x1 + [1]
c_2(x1) = [1] x1 + [0]
c_3(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules:
{ 3^#(c(x1)) -> c_7()
, 3^#(L(x1)) -> c_3(3^#(x1))
, R^#(1(x1)) -> c_2(3^#(x1))}
Details:
The given problem does not contain any strict rules
8) { R^#(1(x1)) -> c_2(3^#(x1))
, 3^#(L(x1)) -> c_3(3^#(x1))}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
R(x1) = [0] x1 + [0]
2(x1) = [0] x1 + [0]
3(x1) = [0] x1 + [0]
1(x1) = [0] x1 + [0]
L(x1) = [0] x1 + [0]
0(x1) = [0] x1 + [0]
b(x1) = [0] x1 + [0]
c(x1) = [0] x1 + [0]
R^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
2^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
3^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {3^#(L(x1)) -> c_3(3^#(x1))}
Weak Rules: {R^#(1(x1)) -> c_2(3^#(x1))}
Details:
We apply the weight gap principle, strictly orienting the rules
{3^#(L(x1)) -> c_3(3^#(x1))}
and weakly orienting the rules
{R^#(1(x1)) -> c_2(3^#(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{3^#(L(x1)) -> c_3(3^#(x1))}
Details:
Interpretation Functions:
R(x1) = [0] x1 + [0]
2(x1) = [0] x1 + [0]
3(x1) = [0] x1 + [0]
1(x1) = [1] x1 + [0]
L(x1) = [1] x1 + [8]
0(x1) = [0] x1 + [0]
b(x1) = [0] x1 + [0]
c(x1) = [0] x1 + [0]
R^#(x1) = [1] x1 + [8]
c_0(x1) = [0] x1 + [0]
2^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
3^#(x1) = [1] x1 + [1]
c_2(x1) = [1] x1 + [1]
c_3(x1) = [1] x1 + [3]
c_4(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules:
{ 3^#(L(x1)) -> c_3(3^#(x1))
, R^#(1(x1)) -> c_2(3^#(x1))}
Details:
The given problem does not contain any strict rules
9) { R^#(1(x1)) -> c_2(3^#(x1))
, 3^#(c(x1)) -> c_7()}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
R(x1) = [0] x1 + [0]
2(x1) = [0] x1 + [0]
3(x1) = [0] x1 + [0]
1(x1) = [0] x1 + [0]
L(x1) = [0] x1 + [0]
0(x1) = [0] x1 + [0]
b(x1) = [0] x1 + [0]
c(x1) = [0] x1 + [0]
R^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
2^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
3^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {3^#(c(x1)) -> c_7()}
Weak Rules: {R^#(1(x1)) -> c_2(3^#(x1))}
Details:
We apply the weight gap principle, strictly orienting the rules
{3^#(c(x1)) -> c_7()}
and weakly orienting the rules
{R^#(1(x1)) -> c_2(3^#(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{3^#(c(x1)) -> c_7()}
Details:
Interpretation Functions:
R(x1) = [0] x1 + [0]
2(x1) = [0] x1 + [0]
3(x1) = [0] x1 + [0]
1(x1) = [1] x1 + [0]
L(x1) = [0] x1 + [0]
0(x1) = [0] x1 + [0]
b(x1) = [0] x1 + [0]
c(x1) = [1] x1 + [0]
R^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
2^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
3^#(x1) = [1] x1 + [1]
c_2(x1) = [1] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules:
{ 3^#(c(x1)) -> c_7()
, R^#(1(x1)) -> c_2(3^#(x1))}
Details:
The given problem does not contain any strict rules
10)
{R^#(1(x1)) -> c_2(3^#(x1))}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
R(x1) = [0] x1 + [0]
2(x1) = [0] x1 + [0]
3(x1) = [0] x1 + [0]
1(x1) = [0] x1 + [0]
L(x1) = [0] x1 + [0]
0(x1) = [0] x1 + [0]
b(x1) = [0] x1 + [0]
c(x1) = [0] x1 + [0]
R^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
2^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
3^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {R^#(1(x1)) -> c_2(3^#(x1))}
Weak Rules: {}
Details:
We apply the weight gap principle, strictly orienting the rules
{R^#(1(x1)) -> c_2(3^#(x1))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{R^#(1(x1)) -> c_2(3^#(x1))}
Details:
Interpretation Functions:
R(x1) = [0] x1 + [0]
2(x1) = [0] x1 + [0]
3(x1) = [0] x1 + [0]
1(x1) = [1] x1 + [0]
L(x1) = [0] x1 + [0]
0(x1) = [0] x1 + [0]
b(x1) = [0] x1 + [0]
c(x1) = [0] x1 + [0]
R^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
2^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
3^#(x1) = [1] x1 + [0]
c_2(x1) = [1] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules: {R^#(1(x1)) -> c_2(3^#(x1))}
Details:
The given problem does not contain any strict rules
11)
{R^#(b(x1)) -> c_6()}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
R(x1) = [0] x1 + [0]
2(x1) = [0] x1 + [0]
3(x1) = [0] x1 + [0]
1(x1) = [0] x1 + [0]
L(x1) = [0] x1 + [0]
0(x1) = [0] x1 + [0]
b(x1) = [0] x1 + [0]
c(x1) = [0] x1 + [0]
R^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
2^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
3^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {R^#(b(x1)) -> c_6()}
Weak Rules: {}
Details:
We apply the weight gap principle, strictly orienting the rules
{R^#(b(x1)) -> c_6()}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{R^#(b(x1)) -> c_6()}
Details:
Interpretation Functions:
R(x1) = [0] x1 + [0]
2(x1) = [0] x1 + [0]
3(x1) = [0] x1 + [0]
1(x1) = [0] x1 + [0]
L(x1) = [0] x1 + [0]
0(x1) = [0] x1 + [0]
b(x1) = [1] x1 + [0]
c(x1) = [0] x1 + [0]
R^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
2^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
3^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules: {R^#(b(x1)) -> c_6()}
Details:
The given problem does not contain any strict rules